Search for: All records

This paper presents the design ofForge, a tool for teaching formal methods gradually. Forge is based on the widely-used Alloy language and analysis tool, but contains numerous improvements based on more than a decade of experience teaching Alloy to students. Although our focus has been on the classroom, many of the ideas in Forge likely also apply to training in industry. Forge offers aprogression of languagesthat improve the learning experience by only gradually increasing in expressive power. Forge supportscustom visualizationof its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety oftesting featuresto ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and then provide a substantial evaluation based on multiple years of classroom use. 

Abstract We develop the analytic theory describing the formation and evolution of entangled quantum states for a fermionic quantum emitter coupled simultaneously to a quantized electromagnetic field in a nanocavity and quantized phonon or mechanical vibrational modes. The theory is applicable to a broad range of cavity quantum optomechanics problems and emerging research on plasmonic nanocavities coupled to single molecules and other quantum emitters. The optimal conditions for a tripartite entanglement are realized near the parametric resonances in a coupled system. The model includes dissipation and decoherence effects due to coupling of the fermion, photon, and phonon subsystems to their dissipative reservoirs within the stochastic evolution approach, which is derived from the Heisenberg–Langevin formalism. Our theory provides analytic expressions for the time evolution of the quantum state and observables and the emission spectra. The limit of a classical acoustic pumping and the interplay between parametric and standard one-photon resonances are analyzed.